PittsburghV1, France, Analysis, bibRecord, 000119

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

Identifieur interne : 000119 ( France/Analysis ); précédent : 000118; suivant : 000120

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

Auteurs : Khalil Ghorbal [France] ; Andrew Sogokon [Royaume-Uni] ; André Platzer [États-Unis]

Source :

RBID : Hal:hal-01232288

English descriptors

mix :
- Deductive Power, Dynamical Systems, Formal Verification, Polynomial Differential Equations, Positive Invariance.

Abstract

This paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.

Url:

https://hal.archives-ouvertes.fr/hal-01232288

DOI: 10.1016/j.cl.2015.11.003

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 000042
to stream Hal, to step Curation: 000042
to stream Hal, to step Checkpoint: 000136
to stream Main, to step Merge: 000174
to stream Main, to step Curation: 000174
to stream Main, to step Exploration: 000174
to stream France, to step Extraction: 000119

Links to Exploration step

Hal:hal-01232288

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets</title>
<author><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-227330" status="OLD">          <idno type="RNSR">201321225U</idno>
          <orgName>Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques</orgName>
          <orgName type="acronym">HYCOMES</orgName>
          <desc>            <address>              <addrLine>Campus de Beaulieu, 35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/hycomes</ref>
          </desc>
          <listRelation>            <relation active="#struct-419153" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-419365" type="direct"></relation>
            <relation active="#struct-105128" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno>
<orgName>Inria Rennes – Bretagne Atlantique </orgName>
<desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/rennes</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="OLD">          <orgName>LANGAGE ET GÉNIE LOGICIEL</orgName>
          <orgName type="acronym">IRISA-D4</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref>
          </desc>
          <listRelation>            <relation active="#struct-105128" type="direct"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="OLD">          <idno type="IdRef">026386909</idno>
          <idno type="ISNI">0000 0001 2298 7270</idno>
          <idno type="RNSR">200012163A</idno>
          <orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName>
          <orgName type="acronym">IRISA</orgName>
          <date type="start">2000</date>
          <date type="end">2016-12-31</date>
          <desc>            <address>              <addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.irisa.fr</ref>
          </desc>
          <listRelation>            <relation active="#struct-172265" type="direct"></relation>
            <relation name="UMR6074" active="#struct-441569" type="direct"></relation>
            <relation active="#struct-247362" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation name="- RENNES" active="#struct-301232" type="direct"></relation>
            <relation active="#struct-301262" type="direct"></relation>
            <relation active="#struct-105160" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID">          <orgName>Université de Bretagne Sud</orgName>
          <orgName type="acronym">UBS</orgName>
          <desc>            <address>              <addrLine>BP 92116 - 56321 Lorient cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-ubs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID">          <orgName>École normale supérieure - Rennes</orgName>
          <orgName type="acronym">ENS Rennes</orgName>
          <desc>            <address>              <addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.ens-rennes.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="institution" xml:id="struct-301232" status="VALID">          <orgName>Institut National des Sciences Appliquées</orgName>
          <orgName type="acronym">INSA</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="VALID">          <orgName>Télécom Bretagne</orgName>
          <date type="start">1977</date>
          <desc>            <address>              <addrLine>Technopôle Brest-IroiseCS 8381829238 BREST Cedex 3</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.telecom-bretagne.eu/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID">          <orgName>Université de Rennes 1</orgName>
          <orgName type="acronym">UR1</orgName>
          <desc>            <address>              <addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-rennes1.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID"><orgName>CentraleSupélec</orgName>
<desc><address><addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.centralesupelec.fr</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Lorient</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Bretagne-Sud</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
<placeName><settlement type="city">Rennes</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Rennes 1</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
</affiliation>
</author>
<author><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </hal:affiliation>
<country>Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01232288</idno>
<idno type="halId">hal-01232288</idno>
<idno type="halUri">https://hal.archives-ouvertes.fr/hal-01232288</idno>
<idno type="url">https://hal.archives-ouvertes.fr/hal-01232288</idno>
<idno type="doi">10.1016/j.cl.2015.11.003</idno>
<date when="2015-11-23">2015-11-23</date>
<idno type="wicri:Area/Hal/Corpus">000042</idno>
<idno type="wicri:Area/Hal/Curation">000042</idno>
<idno type="wicri:Area/Hal/Checkpoint">000136</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000136</idno>
<idno type="wicri:Area/Main/Merge">000174</idno>
<idno type="wicri:Area/Main/Curation">000174</idno>
<idno type="wicri:Area/Main/Exploration">000174</idno>
<idno type="wicri:Area/France/Extraction">000119</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets</title>
<author><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-227330" status="OLD">          <idno type="RNSR">201321225U</idno>
          <orgName>Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques</orgName>
          <orgName type="acronym">HYCOMES</orgName>
          <desc>            <address>              <addrLine>Campus de Beaulieu, 35042 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.inria.fr/equipes/hycomes</ref>
          </desc>
          <listRelation>            <relation active="#struct-419153" type="direct"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation active="#struct-419365" type="direct"></relation>
            <relation active="#struct-105128" type="indirect"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno>
<orgName>Inria Rennes – Bretagne Atlantique </orgName>
<desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/rennes</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="OLD">          <orgName>LANGAGE ET GÉNIE LOGICIEL</orgName>
          <orgName type="acronym">IRISA-D4</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref>
          </desc>
          <listRelation>            <relation active="#struct-105128" type="direct"></relation>
            <relation active="#struct-172265" type="indirect"></relation>
            <relation name="UMR6074" active="#struct-441569" type="indirect"></relation>
            <relation active="#struct-247362" type="indirect"></relation>
            <relation active="#struct-300009" type="indirect"></relation>
            <relation name="- RENNES" active="#struct-301232" type="indirect"></relation>
            <relation active="#struct-301262" type="indirect"></relation>
            <relation active="#struct-105160" type="indirect"></relation>
            <relation active="#struct-411575" type="indirect"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="OLD">          <idno type="IdRef">026386909</idno>
          <idno type="ISNI">0000 0001 2298 7270</idno>
          <idno type="RNSR">200012163A</idno>
          <orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName>
          <orgName type="acronym">IRISA</orgName>
          <date type="start">2000</date>
          <date type="end">2016-12-31</date>
          <desc>            <address>              <addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.irisa.fr</ref>
          </desc>
          <listRelation>            <relation active="#struct-172265" type="direct"></relation>
            <relation name="UMR6074" active="#struct-441569" type="direct"></relation>
            <relation active="#struct-247362" type="direct"></relation>
            <relation active="#struct-300009" type="direct"></relation>
            <relation name="- RENNES" active="#struct-301232" type="direct"></relation>
            <relation active="#struct-301262" type="direct"></relation>
            <relation active="#struct-105160" type="direct"></relation>
            <relation active="#struct-411575" type="direct"></relation>
          </listRelation>
        </org>
</tutelle>
<tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID">          <orgName>Université de Bretagne Sud</orgName>
          <orgName type="acronym">UBS</orgName>
          <desc>            <address>              <addrLine>BP 92116 - 56321 Lorient cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-ubs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID">          <idno type="IdRef">02636817X</idno>
          <idno type="ISNI">0000000122597504</idno>
          <orgName>Centre National de la Recherche Scientifique</orgName>
          <orgName type="acronym">CNRS</orgName>
          <date type="start">1939-10-19</date>
          <desc>            <address>              <country key="FR"></country>
            </address>
            <ref type="url">http://www.cnrs.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID">          <orgName>École normale supérieure - Rennes</orgName>
          <orgName type="acronym">ENS Rennes</orgName>
          <desc>            <address>              <addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.ens-rennes.fr</ref>
          </desc>
        </org>
</tutelle>
<tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="institution" xml:id="struct-301232" status="VALID">          <orgName>Institut National des Sciences Appliquées</orgName>
          <orgName type="acronym">INSA</orgName>
          <desc>            <address>              <country key="FR"></country>
            </address>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="VALID">          <orgName>Télécom Bretagne</orgName>
          <date type="start">1977</date>
          <desc>            <address>              <addrLine>Technopôle Brest-IroiseCS 8381829238 BREST Cedex 3</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.telecom-bretagne.eu/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID">          <orgName>Université de Rennes 1</orgName>
          <orgName type="acronym">UR1</orgName>
          <desc>            <address>              <addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.univ-rennes1.fr/</ref>
          </desc>
        </org>
</tutelle>
<tutelle active="#struct-411575" type="indirect"><org type="institution" xml:id="struct-411575" status="VALID"><orgName>CentraleSupélec</orgName>
<desc><address><addrLine>3, rue Joliot Curie,Plateau de Moulon,91192 GIF-SUR-YVETTE Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.centralesupelec.fr</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Lorient</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Bretagne-Sud</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
<placeName><settlement type="city">Rennes</settlement>
<region type="region" nuts="2">Région Bretagne</region>
</placeName>
<orgName type="university">Université de Rennes 1</orgName>
<orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName>
</affiliation>
</author>
<author><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </hal:affiliation>
<country>Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1016/j.cl.2015.11.003</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Deductive Power</term>
<term>Dynamical Systems</term>
<term>Formal Verification</term>
<term>Polynomial Differential Equations</term>
<term>Positive Invariance</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">This paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Royaume-Uni</li>
<li>États-Unis</li>
</country>
<region><li>Région Bretagne</li>
</region>
<settlement><li>Lorient</li>
<li>Rennes</li>
</settlement>
<orgName><li>Université de Bretagne-Sud</li>
<li>Université de Rennes 1</li>
<li>Université européenne de Bretagne</li>
</orgName>
</list>
<tree><country name="France"><region name="Région Bretagne"><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
</region>
</country>
<country name="Royaume-Uni"><noRegion><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
</noRegion>
</country>
<country name="États-Unis"><noRegion><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/France/Analysis

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000119 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/France/Analysis/biblio.hfd -nk 000119 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Amérique
   |area=    PittsburghV1
   |flux=    France
   |étape=   Analysis
   |type=    RBID
   |clé=     Hal:hal-01232288
   |texte=   A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
}}

This area was generated with Dilib version V0.6.38.
Data generation: Fri Jun 18 17:37:45 2021. Site generation: Fri Jun 18 18:15:47 2021

	Serveur d'exploration sur Pittsburgh
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur Pittsburgh

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

Source :

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri